0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 6 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 InliningProof (UPPER BOUND(ID), 943 ms)
↳12 CpxRNTS
↳13 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CpxRNTS
↳15 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 IntTrsBoundProof (UPPER BOUND(ID), 329 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 44 ms)
↳20 CpxRNTS
↳21 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳22 CpxRNTS
↳23 IntTrsBoundProof (UPPER BOUND(ID), 135 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 7 ms)
↳26 CpxRNTS
↳27 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳28 CpxRNTS
↳29 IntTrsBoundProof (UPPER BOUND(ID), 93 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 7 ms)
↳32 CpxRNTS
↳33 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳34 CpxRNTS
↳35 IntTrsBoundProof (UPPER BOUND(ID), 381 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 227 ms)
↳38 CpxRNTS
↳39 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳40 CpxRNTS
↳41 IntTrsBoundProof (UPPER BOUND(ID), 1402 ms)
↳42 CpxRNTS
↳43 IntTrsBoundProof (UPPER BOUND(ID), 2445 ms)
↳44 CpxRNTS
↳45 FinalProof (⇔, 0 ms)
↳46 BOUNDS(1, n^1)
a(C(x1, x2), y) → C(a(x1, y), a(x2, C(x1, x2)))
a(Z, y) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
a(C(x1, x2), y) → C(a(x1, y), a(x2, C(x1, x2))) [1]
a(Z, y) → Z [1]
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1]
eqZList(C(x1, x2), Z) → False [1]
eqZList(Z, C(y1, y2)) → False [1]
eqZList(Z, Z) → True [1]
second(C(x1, x2)) → x2 [1]
first(C(x1, x2)) → x1 [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]
a(C(x1, x2), y) → C(a(x1, y), a(x2, C(x1, x2))) [1]
a(Z, y) → Z [1]
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1]
eqZList(C(x1, x2), Z) → False [1]
eqZList(Z, C(y1, y2)) → False [1]
eqZList(Z, Z) → True [1]
second(C(x1, x2)) → x2 [1]
first(C(x1, x2)) → x1 [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]
a :: C:Z → C:Z → C:Z C :: C:Z → C:Z → C:Z Z :: C:Z eqZList :: C:Z → C:Z → False:True and :: False:True → False:True → False:True False :: False:True True :: False:True second :: C:Z → C:Z first :: C:Z → C:Z |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
a
second
first
eqZList
and
and(v0, v1) → null_and [0]
null_and
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Z => 0
False => 1
True => 2
null_and => 0
a(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
a(z, z') -{ 1 }→ 1 + a(x1, y) + a(x2, 1 + x1 + x2) :|: x1 >= 0, y >= 0, z = 1 + x1 + x2, z' = y, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(2, 2) :|: z = 1 + 0 + 0, z' = 1 + 0 + 0
eqZList(z, z') -{ 3 }→ and(2, 1) :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0
eqZList(z, z') -{ 3 }→ and(2, 1) :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 3 }→ and(1, 2) :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, 2) :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
a(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
a(z, z') -{ 1 }→ 1 + a(x1, y) + a(x2, 1 + x1 + x2) :|: x1 >= 0, y >= 0, z = 1 + x1 + x2, z' = y, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
{ and } { first } { second } { a } { eqZList } |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: ?, size: O(1) [2] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: ?, size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: ?, size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] a: runtime: ?, size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 1 }→ 1 + a(x1, z') + a(x2, 1 + x1 + x2) :|: x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] a: runtime: O(n1) [1 + 2·z], size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] a: runtime: O(n1) [1 + 2·z], size: O(n1) [z] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] a: runtime: O(n1) [1 + 2·z], size: O(n1) [z] eqZList: runtime: ?, size: O(1) [2] |
a(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
a(z, z') -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z' >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] a: runtime: O(n1) [1 + 2·z], size: O(n1) [z] eqZList: runtime: O(n1) [78 + 156·z'], size: O(1) [2] |